g:GrpSig, b:, x:|g|. ((b))  ((when b. x) = e  |g|) 

latex

Up	groups 1
Definitions of Statement	when b. p
Definitions	, ff, tt, t  T, if b then t else f fi , when b. p, P  Q, x:A. B(x), False, P & Q, P  Q, Unit, A, ,
Lemmas	grp sig wf, grp car wf, grp id wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf